\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{2}


\chapter{Isomorphisms}

When we say that:
\[f \circ (g \circ h) = (f \circ g) \circ h \]
or:
\[ f = f \circ id \]
we are asserting the \emph{equality} of arrows. The arrow on the left is the result of one operation, and the arrow on the right is the result of another. But the results are \emph{equal}.

We often illustrate such equalities by drawing \emph{commuting} diagrams, e.g.,

\[
 \begin{tikzcd}
 a
 \arrow[r, "h"]
 \arrow[rr, bend left=45, "g \circ h"]
 \arrow[rrr, bend left=80, "f \circ (g \circ h)"]
 \arrow[rrr, bend right=80, "(f \circ g) \circ h"]
 & b
 \arrow[r, "g"]
 \arrow[rr, bend right=45, "f \circ g"]
 &c
 \arrow[r, "f"]
 &d
 \end{tikzcd}
 \begin{tikzcd}
 a
 \arrow[r, "f"]
 \arrow[r, loop, "id"']
 &b
 \end{tikzcd}
\]

Thus we compare arrows for equality.

We do \emph{not} compare objects for equality\footnote{Half-jokingly, invoking equality of objects is considered ``evil'' in category theory.}. We see objects as confluences of arrows, so if we want to compare two objects, we look at the arrows.

\section{Isomorphic Objects}

The simplest relation between two objects is an arrow.

The simplest round trip is a composition of two arrows going in opposite directions. 

\[
 \begin{tikzcd}
 a
 \arrow[r, bend left, "f"]
 & b
 \arrow[l, bend left, "g"]
 \end{tikzcd}
\]

There are two possible round trips. One is $g \circ f$, which goes from $a$ to $a$. The other is $f \circ g$ , which goes from $b$ to $b$.

If both of them result in identities, then we say that $g$ is the \emph{inverse} of $f$
\[ g \circ f = id_a\]
\[f \circ g = id_b\]
and we write it as $g = f^{-1}$ (pronounced $f$ \emph{inverse}). The arrow $ f^{-1}$ undoes the work of the arrow $f$. 

Such a pair of arrows is called an \emph{isomorphism} and the two objects are called \emph{isomorphic}.

In programming, two isomorphic types have the same external behavior. One type can be implemented in terms of the other and vice versa. One can be replaced by the other without changing the behavior of the system (except, possibly, the performance). 

In Haskell, we often define types in terms of other types. If it's just a matter of replacing one name by another, we use a type synonym. For instance:
\begin{haskell}
type MyTemperature = Int
\end{haskell}
lets us use \hask{MyTemperature} as a more descriptive name for an integer in a program that deals with weather. These two types are then equal---one can be substituted for another in all contexts, and all functions that accept \hask{Int} arguments can be called with \hask{MyTemperature}.

When we want to define a new type that is \emph{isomorphic} but not equal to an existing type, we can use \index{newtype}\hask{newtype}. For instance, we can define \hask{Temperature} as:
\begin{haskell}
newtype Temperature = Temp Int
\end{haskell}
Here, \hask{Temperature} is the new type and \hask{Temp} is a \emph{data constructor}. A data constructor is just a function\footnote{Unlike with regular functions, the names of data constructors must start with a capital letter}:
\begin{haskell}
Temp :: Int -> Temp
\end{haskell}
We can also define its inverse:
\begin{haskell}
toInt :: Temperature -> Int
toInt (Temp i) = i
\end{haskell}
thus completing the isomorphism:
\[
 \begin{tikzcd}
 \hask{Int}
 \arrow[r, bend left, "\hask{Temp}"]
 & \hask{Temperature}
 \arrow[l, bend left, "\hask{toInt}"]
 \end{tikzcd}
\]
Since this is a common construction, Haskell provides special syntax that defines both functions at once:
\begin{haskell}
newtype Temperature = Temp { toInt :: Int}
\end{haskell}

Because \hask{Temperature} is a new type, functions that operate on integers will not accept it as an argument. This way the programmer can restrict the way it can be used. We can still use the isomorphism to selectively allow some operations, as in this application of the function \hask{negate :: Int -> Int}. The code that does it is the direct translation of the diagram:
\[ \hask{Temperature} \xrightarrow{\hask{toInt}} \hask{Int} \xrightarrow{\hask{negate}} \hask{Int} \xrightarrow{\hask{Temp}} \hask{Temperature} \]
\begin{haskell}
invert :: Temperature -> Temperature
invert = Temp . negate . toInt
\end{haskell}


\subsection{Isomorphism and bijections}

What does the existence of an isomorphism tell us about the two objects it connects? 

We have said that objects are described by their interactions with other objects. So let's consider what the two isomorphic objects look like from the perspective of an observer  $x$. Take an arrow $h$ coming from $x$ to $a$.

\[
 \begin{tikzcd}
 & x
 \arrow[ld, red, "h"']
 \\
 a
 \arrow[rr, "f"]
  && b
 \arrow[ll, bend left,  "f^{-1}"]
 \end{tikzcd}
\]
There is a corresponding arrow coming from $x$ to $b$. It's just the composition of $f \circ h$, or the action of $(f \circ -)$ on $h$.
\[
 \begin{tikzcd}
 & x
 \arrow[ld, "h"']
 \arrow[rd, red, "f \circ h"]
 \\
 a
 \arrow[rr, "f"]
  && b
 \arrow[ll, bend left,  "f^{-1}"]
 \end{tikzcd}
\]
Similarly, for any arrow probing $b$ there is a corresponding arrow probing $a$. It is given by the action of  $(f^{-1} \circ -)$. 

We can move focus back and forth between $a$ and $b$ using the mappings $(f \circ -)$ and $(f^{-1} \circ -)$.

We can combine these two mappings (see exercise \ref{ex-yoneda-composition}) to form a round trip. The result is the same as if we applied the composite $((f^{-1} \circ f) \circ -)$. But this is equal to $(id_a \circ  -)$ which, as we know from exercise \ref{ex-yoneda-identity}, leaves the arrows unchanged.

Similarly, the round trip induced by $f \circ f^{-1}$ leaves the arrows $x \to b$ unchanged. 

This creates a ``buddy system'' between the two groups of arrows. Imagine each arrow sending a message to its buddy, as determined by $f$ or $f^{-1}$. Each arrow would then receive exactly one message, and that would be a message from its buddy. No arrow would be left behind, and no arrow would receive more than one message. Mathematicians call this kind of buddy system a \emph{bijection} or one-to-one correspondence.

Therefore, arrow by arrow, the two objects $a$ and $b$ look exactly the same from the perspective of $x$. Arrow-wise, there is no difference between the two objects. 

Two isomorphic objects have exactly the same properties.

In particular, if you replace $x$ with the terminal object $1$, you'll see that the two objects have the same elements. For every element $x \colon 1 \to a$ there is a corresponding element $y \colon 1 \to b$, namely $y = f \circ x$, and vice versa. There is a bijection between the elements of isomorphic objects.

Such indistinguishable objects are called \emph{isomorphic} because they have ``the same shape.'' You've seen one, you've seen them all. 

We write this isomorphism as:

\[a \cong b\]

When dealing with objects, we use isomorphism in place of equality.

In classical logic, if B follows from A and A follows from B then A and B are logically equivalent. We often say that B is true ``if and only if'' A is true. However, unlike previous parallels between logic and type theory, this one is not as straightforward if you consider proofs to be relevant. In fact, it led to the development of a new branch of fundamental mathematics called homotopy type theory, or HoTT for short.

\begin{exercise}
Make an argument that there is a bijection between arrows that are \emph{outgoing} from two isomorphic objects. Draw the corresponding diagrams.
\end{exercise}


\begin{exercise}
Show that every object is isomorphic to itself
\end{exercise}

\begin{exercise}
If there are two terminal objects, show that they are isomorphic
\end{exercise}

\begin{exercise}
Show that the isomorphism from the previous exercise is unique.
\end{exercise}

\section{Naturality}

We've seen that, when two objects are isomorphic, we can switch focus from one to another using post-composition: either $(f \circ -)$ or $(f^{-1} \circ -)$. 

Conversely, to switch between different observers, we would use pre-composition. 

Indeed, an arrow $h$ probing $a$ from $x$ is related to the arrow $h\circ g$ probing the same object from $y$.

\[
 \begin{tikzcd}
 x
 \arrow[d, "h"']
 && y
 \arrow[ll, dashed, "g"']
  \arrow[dll, red, "h \circ g"']
 \\
 a
 \arrow[rr, "f"]
  && b
 \arrow[ll, bend left,  "f^{-1}"]
 \end{tikzcd}
\]
Similarly, an arrow $h'$ probing $b$ from $x$ corresponds to the arrow $h' \circ g$ probing it from $y$. 

\[
 \begin{tikzcd}
 x
 \arrow[drr, "h'"]
 && y
 \arrow[ll, dashed, "g"']
  \arrow[d, red, "h' \circ g"]
 \\
 a
 \arrow[rr, "f"]
  && b
 \arrow[ll, bend left,  "f^{-1}"]
 \end{tikzcd}
\]
In both cases, we change perspective from $x$ to $y$ by applying precomposition $(- \circ g)$.

The important observation is that the change of perspective preserves the buddy system established by the isomorphism. If two arrows were buddies from the perspective of $x$, they are still buddies from the perspective of $y$. This is as simple as saying that it doesn't matter if you first pre-compose with $g$ (switch perspective) and then post-compose with $f$ (switch focus), or first post-compose with $f$ and then pre-compose with $g$. Symbolically, we write it as:

\[(- \circ g) \circ (f \circ -) = (f \circ -) \circ (- \circ g)\]
and we call it the \emph{naturality} condition.


The meaning of this equation is revealed when you apply it to a morphism $h \colon x \to a$. Both sides evaluate to $f \circ h \circ g$.
\[
 \begin{tikzcd}
 h
 \arrow[r, mapsto, "(- \circ g)"]
 \arrow[d, mapsto, "(f \circ -)"']
 & h \circ g
 \arrow[d, mapsto, "(f \circ -)"]
 \\
 f \circ h
 \arrow[r, mapsto, "(- \circ g)"]
& f \circ h \circ g
 \end{tikzcd}
\]

Here, the naturality condition is satisfied automatically due to associativity, but we'll soon see it generalized to less trivial circumstances.


Arrows are used to broadcast information about an isomorphism. Naturality tells us that all objects get a consistent view of it, independent of the path. 

We can also reverse the roles of observers and subjects. For instance, using an arrow $h \colon a \to x$, the object $a$ can probe an arbitrary object $x$. If there is an arrow $g \colon x \to y$, it can switch focus to $y$. Switching the perspective to $b$ is done by precomposition with $f^{-1}$.
\[
 \begin{tikzcd}
 a
 \arrow[rr, "f"]
 \arrow[d, "h"']
 \arrow[rrd, red, "g\circ h"]
 && b
  \arrow[ll, bend right,  "f^{-1}"']
 \\
 x
 \arrow[rr, dashed, "g"']
  && y
 \end{tikzcd}
\]
Again, we have the naturality condition, this time from the point of view of the isomorphic pair:
\[(- \circ f^{-1}) \circ (g \circ -) = (g \circ -) \circ (- \circ f^{-1}) \]

This situation when we have to take two steps to move from one place to another is typical in category theory. Here, the operations of pre-composition and post-composition can be done in any order---we say that they \index{commuting operations}\emph{commute}. But in general the order in which we take steps leads to different outcomes. We often impose commutation conditions and say that one operation is compatible with another if these conditions hold.

\begin{exercise}
Show that both sides of the naturality condition for $f^{-1}$, when acting on $h$, reduce to:
\[
 \begin{tikzcd}
 b \arrow[r, "f^{-1}"] &a \arrow[r, "h"] & x \arrow[r, "g"] & y
\end{tikzcd}
\]

\end{exercise}

\section{Reasoning with Arrows}

Master Yoneda says: ``At the arrows look!''

If two objects are isomorphic, they have the same sets of incoming arrows. 

If two objects are isomorphic, they also have the same sets of outgoing arrows.

If you want to see if two objects are isomorphic, at the arrows look!

\medskip

When two objects $a$ and $b$ are isomorphic, any isomorphism $f$ induces a one-to-one mapping $(f \circ -)$ between corresponding sets of arrows.  
\[
 \begin{tikzcd}
 \node(x) at (0, 2) {x};
 \node(a) at (-2, 0) {a};
 \node(b) at (2, 0) {b};
 \node(c1) at (-1, 1.5) {};
 \node(c2) at (-1.5, 1) {};
 \node(c3) at (-1, 2) {};
 \node(c4) at (-2, 1) {};
 \node(d1) at (1, 1.5) {};
 \node(d2) at (1.5, 1) {};
 \node(d3) at (1, 2) {};
 \node(d4) at (2, 1) {};
\node (aa) at (-1, 0.75) {};
 \node (bb) at (1, 0.75) {};
 \draw[->] (x) .. controls (c1)  and (c2) .. (a); % bend
 \draw[->, green] (x) .. controls (c3)  and (c4) .. (a); % bend
 \draw[->, blue] (x) -- (a); 
  \draw[->] (x) .. controls (d1)  and (d2) .. (b); % bend
 \draw[->, green] (x) .. controls (d3)  and (d4) .. (b); % bend
 \draw[->, blue] (x) -- (b); 
 \draw[->, red, dashed] (aa) -- node[above]{(f \circ -)} (bb);
\draw[->] (a) -- node[below]{f} (b);
 \end{tikzcd}
\]
The function $(f \circ -)$ maps every arrow $h \colon x \to a$ to an arrow $f \circ h \colon x \to b$. It's inverse $(f^{-1} \circ -)$ maps every arrow $h' \colon x \to b$ to an arrow $(f^{-1} \circ h')$.


Suppose that we don't know if the objects are isomorphic, but we know that there is an invertible mapping, $\alpha_x$, between sets of arrows impinging on $a$ and $b$ from every object $x$. In other words, for every $x$, $\alpha_x$ is a bijection of arrows. 
\[
 \begin{tikzcd}
 \node(x) at (0, 2) {x};
 \node(a) at (-2, 0) {a};
 \node(b) at (2, 0) {b};
 \node(c1) at (-1, 1.5) {};
 \node(c2) at (-1.5, 1) {};
 \node(c3) at (-1, 2) {};
 \node(c4) at (-2, 1) {};
 \node(d1) at (1, 1.5) {};
 \node(d2) at (1.5, 1) {};
 \node(d3) at (1, 2) {};
 \node(d4) at (2, 1) {};
\node (aa) at (-1, 0.75) {};
 \node (bb) at (1, 0.75) {};
 \draw[->] (x) .. controls (c1)  and (c2) .. (a); % bend
 \draw[->, green] (x) .. controls (c3)  and (c4) .. (a); % bend
 \draw[->, blue] (x) -- (a); 
  \draw[->] (x) .. controls (d1)  and (d2) .. (b); % bend
 \draw[->, green] (x) .. controls (d3)  and (d4) .. (b); % bend
 \draw[->, blue] (x) -- (b); 
 \draw[->, red, dashed] (aa) -- node[above]{\alpha_x} (bb);
 \end{tikzcd}
\]
Before, the bijection of arrows was generated by the isomorphism $f$. Now, the bijection of arrows is given to us by $\alpha_x$. Does it mean that the two objects are isomorphic? Can we construct the isomorphism $f$ from the family of mappings $\alpha_x$? The answer is ``yes'', as long as the family $\alpha_x$ satisfies the naturality condition.

Here's the action of $\alpha_x$ on a particular arrow $h$. 
\[
 \begin{tikzcd}
 x
 \arrow[d, "h"']
 \arrow[rrd, red, "\alpha_x h"]
  \\
 a
  && b
 \end{tikzcd}
\]
This mapping, along with its inverse $\alpha^{-1}_x$, which takes arrows $x \to b$ to arrows $x \to a$, would play the role of $(f \circ -)$ and $(f^{-1} \circ -)$, if there was indeed an isomorphism $f$. The family of maps $\alpha$ describes an ``artificial'' way of switching focus from $a$ to $b$.

Here's the same situation from the point of view of another observer $y$:
\[
 \begin{tikzcd}
 x
  && y
 \arrow[lld, "h'"']
 \arrow[d, red, "\alpha_y h'"]
 \\
 a
  && b
 \end{tikzcd}
\]
Notice that $y$ is using a different mapping $\alpha_y$ from the same family. 

These two mappings, $\alpha_x$ and $\alpha_y$, become entangled whenever there is a morphism $g \colon y \to x$. In that case, pre-composition with $g$ allows us to switch perspective from $x$ to $y$ (notice the direction)

\[
 \begin{tikzcd}
 x
 \arrow[d, "h"']
 && y
 \arrow[ll, dashed, "g"']
 \arrow[lld, red, "h \circ g"]
 \\
 a
  && b
 \end{tikzcd}
\]
We have separated the switching of focus from the switching of perspective. The former is done by $\alpha$, the latter by pre-composition. Naturality imposes a compatibility condition between those two.

Indeed, starting with some $h$, we can either apply $(- \circ g)$ to switch to $y$'s point of view, and then apply $\alpha_y$ to switch focus to $b$:
\[ \alpha_y \circ (- \circ g) \]
or we can first let $x$ switch focus to $b$ using $\alpha_x$, and then switch perspective using $(- \circ g)$:
\[ (- \circ g) \circ \alpha_x \]
In both cases we end up looking at $b$ from $y$. We've done this exercise before, when we had an isomorphism between $a$ and $b$, and we've found out that the results were the same. We called it the naturality condition. 

If we want the $\alpha$'s to give us an isomorphism, we have to impose the equivalent naturality condition:
\[ \alpha_y \circ (- \circ g) = (- \circ g) \circ \alpha_x \]
When acting on some arrow $h \colon x \to a$, we want this diagram to commute:
\[
 \begin{tikzcd}
 h
 \arrow[r, mapsto, "(- \circ g)"]
 \arrow[d, mapsto, red, "\alpha_x"]
 & h \circ g
 \arrow[d, mapsto, red, "\alpha_y"]
 \\
 \alpha_x h
 \arrow[r, mapsto, "(- \circ g)"]
&(\alpha_x h) \circ g = \alpha_y (h \circ g)
 \end{tikzcd}
\]
This way we know that replacing all $\alpha$'s with $(f \circ -)$ will work. But does such $f$ exist? Can we reconstruct $f$ from the $\alpha$'s? The answer is yes, and we'll use the Yoneda trick to accomplish that.

Since $\alpha_x$ is defined for any object $x$, it is also defined for $a$ itself. By definition, $\alpha_a$ takes a morphism $a \to a$ to a morphism $a \to b$. We know for sure that there is at least one morphism $a \to a$, namely the identity $id_a$. It turns out that the isomorphism $f$ we are seeking is given by:
\[f = \alpha_a (id_a)\]
or, pictorially:
\[
 \begin{tikzcd}
a
 \arrow[d, "id_a"']
 \arrow[rrd, red, "f = \alpha_a (id_a)"]
  \\
 a
  && b
 \end{tikzcd}
\]

Let's verify this. If $f$ is indeed our isomorphism then, for any $x$, $\alpha_x$ should be equal to  $(f \circ -)$. To see that, let's rewrite the naturality condition replacing $x$ with $a$. We get:
\[\alpha_y(h \circ g) = (\alpha_a h) \circ g \]
as illustrated in the following diagram:
\[
 \begin{tikzcd}
 a
 \arrow[d, "h"']
 \arrow[rrd,  red, "\alpha_a (h)"']
 && y
 \arrow[ll, "g"']
 \arrow[d, red, "\alpha_y (h \circ g)"]
   \\
 a
  && b
 \end{tikzcd}
\]


Since both the source and the target of $h$ is $a$, this equality must also be true for $h = id_a$
\[\alpha_y (id_a \circ g) = (\alpha_a (id_a)) \circ g \]
But $id_a \circ g$ is equal to $g$ and $\alpha_a(id_a)$ is our $f$, so we get:
\[\alpha_y g = f \circ g = (f \circ -) g\]
In other words, $\alpha_y = (f \circ -)$ for every object $y$ and every morphism $g \colon y \to a$.

Notice that, even though $\alpha_x$ was defined individually for every $x$ and every arrow $x \to a$, it turned out to be completely determined by its value at a single identity arrow. This is the power of naturality!
\subsection{Reversing the Arrows}
As Lao Tzu would say, the duality between the observer and the observed cannot be complete unless the observer is allowed to switch roles with the observed. 

Again, we want to show that two objects $a$ and $b$ are isomorphic, but this time we want to treat them as observers. An arrow $h \colon a \to x$ probes an arbitrary object $x$ from the perspective of $a$. Previously, when we knew that the two objects were isomorphic, we were able to switch perspective to $b$ using $(- \circ f^{-1})$. This time we have at our disposal a transformation $\beta_x$ instead. It establishes the bijection between arrows impinging on $x$.
\[
 \begin{tikzcd}
 x
 \\
 a
\arrow[u, "h"]
 && b
  \arrow[llu, red, "\beta_x h"']
  \end{tikzcd}
\]
If we want to observe another object, $y$, we will use $\beta_y$ to switch perspectives between $a$ and $b$, and so on. 

\[
 \begin{tikzcd}
 \node(x) at (0, 2) {x};
 \node(a) at (-2, 0) {a};
 \node(b) at (2, 0) {b};
 \node(c1) at (-1, 1.5) {};
 \node(c2) at (-1.5, 1) {};
 \node(c3) at (-1, 2) {};
 \node(c4) at (-2, 1) {};
 \node(d1) at (1, 1.5) {};
 \node(d2) at (1.5, 1) {};
 \node(d3) at (1, 2) {};
 \node(d4) at (2, 1) {};
\node (aa) at (-1, 0.75) {};
 \node (bb) at (1, 0.75) {};
 \draw[<-] (x) .. controls (c1)  and (c2) .. (a); % bend
 \draw[<-, green] (x) .. controls (c3)  and (c4) .. (a); % bend
 \draw[<-, blue] (x) -- (a); 
  \draw[<-] (x) .. controls (d1)  and (d2) .. (b); % bend
 \draw[<-, green] (x) .. controls (d3)  and (d4) .. (b); % bend
 \draw[<-, blue] (x) -- (b); 
 \draw[->, red, dashed] (aa) -- node[above]{\beta_x} (bb);
 \end{tikzcd}
\]


If the two objects $x$ and $y$ are connected by an arrow $g \colon x \to y$ then we also have an option of switching focus using $(g \circ -)$. If we want to do both: switch perspective and switch focus, there are two ways of doing it. Naturality demands that the results be equal:
\[ (g \circ -) \circ \beta_x = \beta_y \circ (g \circ -) \]
Indeed, if we replace $\beta$ with $(- \circ f^{-1})$, we recover the naturality condition for an isomorphism. 

\begin{exercise}
Use the trick with the identity morphism to recover $f^{-1}$ from the family of mappings $\beta$.
\end{exercise}
\begin{exercise}
Using $f^{-1}$ from the previous exercise, evaluate $\beta_y g$ for an arbitrary object $y$ and an arbitrary arrow $g \colon a \to y$.
\end{exercise}


As Lao Tzu would say: To show an isomorphism, it is often easier to define a natural transformation between ten thousand arrows than it is to find a pair of arrows between two objects.

\end{document}
